--- /dev/null
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function trywith {
+ ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+ (read result w1;
+ case "$result" in
+ unsat) echo "$w1";cat;exit 0;;
+ esac; exit 1)
+ if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+trywith --cegqi --cegqi-si-multi-inst-abort --cegqi-si-abort --decision=internal
+trywith --cegqi --no-cegqi-si
+
if( !d_syntax_guided ){
//add immediate lemma
Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
- Trace("cegqi") << "Add candidate lemma : " << lem << std::endl;
+ Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl;
qe->getOutputChannel().lemma( lem );
}else if( d_ceg_si ){
- Node lem = d_ceg_si->getSingleInvLemma( d_guard );
- if( !lem.isNull() ){
- Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
- qe->getOutputChannel().lemma( lem );
+ std::vector< Node > lems;
+ d_ceg_si->getSingleInvLemma( d_guard, lems );
+ for( unsigned i=0; i<lems.size(); i++ ){
+ Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl;
+ qe->getOutputChannel().lemma( lems[i] );
if( Trace.isOn("cegqi-debug") ){
- lem = Rewriter::rewrite( lem );
- Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+ Node rlem = Rewriter::rewrite( lems[i] );
+ Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
}
}
}
if( !lems.empty() ){
d_last_inst_si = true;
for( unsigned j=0; j<lems.size(); j++ ){
- Trace("cegqi-lemma") << "Single invocation lemma : " << lems[j] << std::endl;
+ Trace("cegqi-lemma") << "Single invocation instantiation lemma : " << lems[j] << std::endl;
d_quantEngine->addLemma( lems[j] );
}
d_statistics.d_cegqi_si_lemmas += lems.size();
d_sol = new CegConjectureSingleInvSol( qe );
}
-Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
+void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) {
if( !d_single_inv.isNull() ) {
d_single_inv_var.clear();
d_single_inv_sk.clear();
inst = TermDb::simpleNegate( inst );
Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
- //copy variables to instantiator
- d_cinst->d_vars.clear();
- d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
-
- return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
- }else{
- return Node::null();
+ //register with the instantiator
+ Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
+ lems.push_back( ginst );
+ d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
}
}
std::map< Node, Node > d_trans_post;
std::map< Node, std::vector< Node > > d_prog_templ_vars;
public:
- //get the single invocation lemma
- Node getSingleInvLemma( Node guard );
+ //get the single invocation lemma(s)
+ void getSingleInvLemma( Node guard, std::vector< Node >& lems );
//initialize
void initialize( Node q );
//check
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Implementation of cbqi instantiation strategies
+ ** \brief Implementation of counterexample-guided quantifier instantiation strategies
**/
#include "theory/quantifiers/inst_strategy_cbqi.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/first_order_model.h"
+#include "util/ite_removal.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
using namespace CVC4::theory::arith;
-using namespace CVC4::theory::datatypes;
#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
//#define MBP_STRICT_ASSERTIONS
subs_rhs.push_back( r );
}
+void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+ Assert( d_vars.empty() );
+ d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
+ IteSkolemMap iteSkolemMap;
+ d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
+ Assert( d_aux_vars.empty() );
+ for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
+ Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl;
+ d_aux_vars.push_back( i->first );
+ }
+ for( unsigned i=0; i<lems.size(); i++ ){
+ Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl;
+ Node rlem = lems[i];
+ rlem = Rewriter::rewrite( rlem );
+ Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+ //record the literals that imply auxiliary variables to be equal to terms
+ if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
+ if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
+ if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){
+ Node v = lems[i][1][0];
+ for( unsigned r=1; r<=2; r++ ){
+ d_aux_eq[rlem[r]][v] = lems[i][r][1];
+ Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
+ }
+ }
+ }
+ }
+ lems[i] = rlem;
+ }
+}
+
//old implementation
InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
if( it==d_cinst.end() ){
CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
- for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
- cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
- }
d_cinst[q] = cinst;
return cinst;
}else{
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief instantiator_arith_instantiator
+ ** \brief counterexample-guided quantifier instantiation
**/
#include "cvc4_private.h"
-#ifndef __CVC4__INST_STRATEGT_CBQI_H
-#define __CVC4__INST_STRATEGT_CBQI_H
+#ifndef __CVC4__INST_STRATEGY_CBQI_H
+#define __CVC4__INST_STRATEGY_CBQI_H
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/arith/arithvar.h"
class TheoryArith;
}
-namespace datatypes {
- class TheoryDatatypes;
-}
-
namespace quantifiers {
class CegqiOutput
std::map< Node, std::vector< Node > > d_curr_eqc;
std::map< Node, Node > d_curr_rep;
std::vector< Node > d_curr_arith_eqc;
+ //auxiliary variables
+ std::vector< Node > d_aux_vars;
+ //literals to equalities for aux vars
+ std::map< Node, std::map< Node, Node > > d_aux_eq;
+ //the CE variables
+ std::vector< Node > d_vars;
private:
//for adding instantiations during check
void computeProgVars( Node n );
void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
public:
CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
- //the CE variables
- std::vector< Node > d_vars;
- //auxiliary variables
- std::vector< Node > d_aux_vars;
- //literals to equalities for aux vars
- std::map< Node, std::map< Node, Node > > d_aux_eq;
//check : add instantiations based on valuation of d_vars
bool check();
//presolve for quantified formula
void presolve( Node q );
+ //register the counterexample lemma (stored in lems), modify vector
+ void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars );
};
class InstStrategySimplex : public InstStrategy{
#include "theory/quantifiers/inst_strategy_e_matching.h"
#include "theory/quantifiers/inst_strategy_cbqi.h"
#include "theory/quantifiers/trigger.h"
-#include "util/ite_removal.h"
using namespace std;
using namespace CVC4;
lem = Rewriter::rewrite( lem );
Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
- //must explicitly remove ITEs so that we record dependencies
- IteSkolemMap iteSkolemMap;
- std::vector< Node > lems;
- lems.push_back( lem );
- d_quantEngine->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
- CegInstantiator * cinst = NULL;
if( d_i_cegqi ){
- cinst = d_i_cegqi->getInstantiator( f );
- Assert( cinst->d_aux_vars.empty() );
- for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
- Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl;
- cinst->d_aux_vars.push_back( i->first );
+ //must register with the instantiator
+ //must explicitly remove ITEs so that we record dependencies
+ std::vector< Node > ce_vars;
+ for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+ ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
}
- }
- for( unsigned i=0; i<lems.size(); i++ ){
- Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl;
- if( !cinst ){
+ std::vector< Node > lems;
+ lems.push_back( lem );
+ CegInstantiator * cinst = d_i_cegqi->getInstantiator( f );
+ cinst->registerCounterexampleLemma( lems, ce_vars );
+ for( unsigned i=0; i<lems.size(); i++ ){
+ Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl;
d_quantEngine->addLemma( lems[i], false );
- }else{
- Node rlem = lems[i];
- rlem = Rewriter::rewrite( rlem );
- Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
- d_quantEngine->addLemma( rlem, false );
- //record the literals that imply auxiliary variables to be equal to terms
- if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
- if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
- if( std::find( cinst->d_aux_vars.begin(), cinst->d_aux_vars.end(), lems[i][1][0] )!=cinst->d_aux_vars.end() ){
- Node v = lems[i][1][0];
- for( unsigned r=1; r<=2; r++ ){
- cinst->d_aux_eq[rlem[r]][v] = lems[i][r][1];
- Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
- }
- }
- }
- }
}
+ }else{
+ Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
+ d_quantEngine->addLemma( lem, false );
}
-
addedLemma = true;
}
}
bool flag = false;
unsigned n1 = node[0].getNumChildren();
unsigned n2 = node[1].getNumChildren();
- if(n1 - n2) {
- for(unsigned i=0; i<=n1 - n2; i++) {
+ if( n1>n2 ){
+ unsigned diff = n1-n2;
+ for(unsigned i=0; i<diff; i++) {
if(node[0][i] == node[1][0]) {
flag = true;
for(unsigned j=1; j<n2; j++) {
projects / cvc5.git / commitdiff