Assert( q.getKind()==FORALL );
Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
d_quant = q;
+ NodeManager* nm = NodeManager::currentNM();
// pre-simplify the quantified formula based on the process utility
d_simp_quant = d_ceg_proc->preSimplify(d_quant);
}
// initialize the guard
- if (d_ceg_si->getGuard().isNull())
+ d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
+ d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
+ d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
+ AlwaysAssert(!d_feasible_guard.isNull());
+ // this must be called, both to ensure that the feasible guard is
+ // decided on with true polariy, but also to ensure that output channel
+ // has been used on this call to check.
+ d_qe->getOutputChannel().requirePhase(d_feasible_guard, true);
+
+ if (isSingleInvocation())
{
std::vector< Node > lems;
- d_ceg_si->getInitialSingleInvLemma( lems );
+ d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems);
for( unsigned i=0; i<lems.size(); i++ ){
Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
d_qe->getOutputChannel().lemma( lems[i] );
}
}
}
- Assert( !getGuard().isNull() );
- Node gneg = getGuard().negate();
+ Node gneg = d_feasible_guard.negate();
for( unsigned i=0; i<guarded_lemmas.size(); i++ ){
- Node lem = NodeManager::currentNM()->mkNode( OR, gneg, guarded_lemmas[i] );
+ Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl;
d_qe->getOutputChannel().lemma( lem );
}
Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
}
-Node CegConjecture::getGuard() { return d_ceg_si->getGuard(); }
+Node CegConjecture::getGuard() const { return d_feasible_guard; }
bool CegConjecture::isSingleInvocation() const {
return d_ceg_si->isSingleInvocation();
bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
return false;
- }else{
- bool value;
- Assert( !getGuard().isNull() );
- // non or fully single invocation : look at guard only
- if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) {
- if( !value ){
- Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
- return false;
- }
- }else{
- Assert( false );
+ }
+ bool value;
+ Assert(!d_feasible_guard.isNull());
+ // non or fully single invocation : look at guard only
+ if (d_qe->getValuation().hasSatValue(d_feasible_guard, value))
+ {
+ if (!value)
+ {
+ Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+ return false;
}
- return true;
}
+ else
+ {
+ Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard
+ << " is not assigned!" << std::endl;
+ Assert(false);
+ }
+ return true;
}
Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
// first, must try the guard
// which denotes "this conjecture is feasible"
- Node feasible_guard = getGuard();
+ Node feasible_guard = d_feasible_guard;
bool value;
if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) {
priority = 0;
* module to get synthesis solutions.
*/
void getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation);
- /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */
- Node getGuard();
+ /**
+ * The feasible guard whose semantics are "this conjecture is feasiable".
+ * This is "G" in Figure 3 of Reynolds et al CAV 2015.
+ */
+ Node getGuard() const;
/** is ground */
bool isGround() { return d_inner_vars.empty(); }
/** are we using single invocation techniques */
private:
/** reference to quantifier engine */
QuantifiersEngine * d_qe;
+ /** The feasible guard. */
+ Node d_feasible_guard;
/** single invocation utility */
std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
/** utility for static preprocessing and analysis of conjectures */
d_waiting_conj = Node::null();
if (!d_conj->isAssigned())
{
- if (!assignConjecture(q))
- {
- return;
- }
+ assignConjecture(q);
+ // assign conjecture always uses the output channel, we return and
+ // re-check here.
+ return;
}
}
unsigned echeck =
d_sip(new SingleInvocationPartition),
d_sol(new CegConjectureSingleInvSol(qe)),
d_cosi(new CegqiOutputSingleInv(this)),
- d_cinst(NULL),
+ d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)),
d_c_inst_match_trie(NULL),
- d_single_invocation(false) {
- // third and fourth arguments set to (false,false) until we have solution
- // reconstruction for delta and infinity
- d_cinst = new CegInstantiator(d_qe, d_cosi, false, false);
+ d_single_invocation(false)
+{
+ // The third and fourth arguments of d_cosi set to (false,false) until we have
+ // solution reconstruction for delta and infinity.
if (options::incrementalSolving()) {
d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext());
if (d_c_inst_match_trie) {
delete d_c_inst_match_trie;
}
- delete d_cinst;
delete d_cosi;
delete d_sol; // (new CegConjectureSingleInvSol(qe)),
delete d_sip; // d_sip(new SingleInvocationPartition),
}
-void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) {
- Assert( d_si_guard.isNull() );
- //single invocation guard
- d_si_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
- d_si_guard = d_qe->getValuation().ensureLiteral( d_si_guard );
- AlwaysAssert( !d_si_guard.isNull() );
- d_qe->getOutputChannel().requirePhase( d_si_guard, true );
-
- if( !d_single_inv.isNull() ) {
- //make for new var/sk
- d_single_inv_var.clear();
- d_single_inv_sk.clear();
- Node inst;
- if( d_single_inv.getKind()==FORALL ){
- for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
- std::stringstream ss;
- ss << "k_" << d_single_inv[0][i];
- Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
- d_single_inv_var.push_back( d_single_inv[0][i] );
- d_single_inv_sk.push_back( k );
- d_single_inv_sk_index[k] = i;
- }
- inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
- }else{
- inst = d_single_inv;
- }
- inst = TermUtil::simpleNegate( inst );
- Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
-
- //register with the instantiator
- Node ginst = NodeManager::currentNM()->mkNode( OR, d_si_guard.negate(), inst );
- lems.push_back( ginst );
- //make and register the instantiator
- if( d_cinst ){
- delete d_cinst;
+void CegConjectureSingleInv::getInitialSingleInvLemma(Node g,
+ std::vector<Node>& lems)
+{
+ Assert(!g.isNull());
+ Assert(!d_single_inv.isNull());
+ // make for new var/sk
+ d_single_inv_var.clear();
+ d_single_inv_sk.clear();
+ Node inst;
+ NodeManager* nm = NodeManager::currentNM();
+ if (d_single_inv.getKind() == FORALL)
+ {
+ for (unsigned i = 0, size = d_single_inv[0].getNumChildren(); i < size; i++)
+ {
+ std::stringstream ss;
+ ss << "k_" << d_single_inv[0][i];
+ Node k = nm->mkSkolem(ss.str(),
+ d_single_inv[0][i].getType(),
+ "single invocation function skolem");
+ d_single_inv_var.push_back(d_single_inv[0][i]);
+ d_single_inv_sk.push_back(k);
+ d_single_inv_sk_index[k] = i;
}
- d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
- d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
+ inst = d_single_inv[1].substitute(d_single_inv_var.begin(),
+ d_single_inv_var.end(),
+ d_single_inv_sk.begin(),
+ d_single_inv_sk.end());
}
+ else
+ {
+ inst = d_single_inv;
+ }
+ inst = TermUtil::simpleNegate(inst);
+ Trace("cegqi-si") << "Single invocation initial lemma : " << inst
+ << std::endl;
+
+ // register with the instantiator
+ Node ginst = nm->mkNode(OR, g.negate(), inst);
+ lems.push_back(ginst);
+ // make and register the instantiator
+ d_cinst.reset(new CegInstantiator(d_qe, d_cosi, false, false));
+ d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk);
}
void CegConjectureSingleInv::initialize( Node q ) {
// the instantiator's output channel
CegqiOutputSingleInv* d_cosi;
// the instantiator
- CegInstantiator* d_cinst;
+ std::unique_ptr<CegInstantiator> d_cinst;
// list of skolems for each argument of programs
std::vector<Node> d_single_inv_arg_sk;
bool d_single_invocation;
// single invocation portion of quantified formula
Node d_single_inv;
- Node d_si_guard;
// transition relation version per program
std::map< Node, Node > d_trans_pre;
std::map< Node, Node > d_trans_post;
// get simplified conjecture
Node getSimplifiedConjecture() { return d_simp_quant; }
- // get single invocation guard
- Node getGuard() { return d_si_guard; }
public:
- //get the single invocation lemma(s)
- void getInitialSingleInvLemma( std::vector< Node >& lems );
+ /** get the single invocation lemma(s)
+ *
+ * This adds lemmas to lem that initializes this class for doing
+ * counterexample-guided instantiation for the synthesis conjecture. These
+ * lemmas correspond to the negation of the body of the (anti-skolemized)
+ * form of the conjecture for fresh skolems.
+ *
+ * Argument g is guard, for which all the above lemmas are guarded.
+ */
+ void getInitialSingleInvLemma(Node g, std::vector<Node>& lems);
// initialize this class for synthesis conjecture q
void initialize( Node q );
/** finish initialize
projects / cvc5.git / commitdiff