24 #ifndef _cvc3__include__theory_quant_h_
25 #define _cvc3__include__theory_quant_h_
34 class QuantProofRules;
55 std::vector<Expr>
bvs;
70 std::vector<Expr>
getBVs();
174 bool hasMacros(
const std::vector<Expr>& asserts);
317 std::vector<Expr>& varReplacements);
480 int loc_gterm(
const std::vector<Expr>& border,
485 const std::vector<Expr>& mtrigs,
487 std::vector<std::vector<Expr> >& instSet,
488 std::vector<Expr>& cur_inst
492 const std::vector<Expr>& border,
493 std::vector<std::vector<Expr> >& instSet
547 void enqueueInst(
size_t univ_id ,
const std::vector<Expr>& bind,
const Expr& gterm);
550 const std::vector<Expr>& binds,
559 bool insted(
const Theorem & univ,
const std::vector<Expr>& binds);
568 void synNewInst(
size_t univ_id,
const std::vector<Expr>& binds,
const Expr& gterm,
const Trigger& trig );
577 const std::vector<Expr> & boundVars,
578 std::vector<std::vector<Expr> >& instBindsTerm,
579 std::vector<Expr>& instGterm,
583 const std::vector<Expr> & boundVars,
584 std::vector<std::vector<Expr> >& instBinds,
585 std::vector<Expr>& instGterms,
590 const std::vector<Expr> & boundVars,
591 std::vector<std::vector<Expr> >& instBinds,
592 std::vector<Expr>& instGterms,
649 std::vector<Expr> & boundVars,
650 std::vector<std::vector<Expr> >& instBinds,
651 std::vector<Expr>& instGterms,
656 const std::vector<Expr> & boundVars,
657 std::vector<std::vector<Expr> >& instBinds,
658 std::vector<Expr>& instGterms,
664 std::vector<Expr>& bVars,
665 std::vector<std::vector<Expr> >& instSet,
670 const std::vector<Expr>& bVars,
671 std::vector<Expr>& newInst,
672 std::set<std::vector<Expr> >& instSet);
675 std::vector<Expr>& bVars,
676 std::set<std::vector<Expr> >& instSet,
679 bool isTransLike (
const std::vector<Expr>& cur_trig);
695 const std::vector<Expr> thmBVs,