theory/quantifiers/fun_def_process.h \
theory/quantifiers/fun_def_process.cpp \
theory/quantifiers/fun_def_engine.h \
- theory/quantifiers/fun_def_engine.cpp \
+ theory/quantifiers/fun_def_engine.cpp \
+ theory/quantifiers/quant_equality_engine.h \
+ theory/quantifiers/quant_equality_engine.cpp \
theory/quantifiers/options_handlers.h \
theory/arith/theory_arith_type_rules.h \
theory/arith/type_enumerator.h \
// Dump the assertions
dumpAssertions("pre-everything", d_assertions);
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl;
Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// Assertions are NOT guaranteed to be rewritten by this point
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl;
dumpAssertions("pre-definition-expansion", d_assertions);
{
Chat() << "expanding definitions..." << endl;
d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
}
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
dumpAssertions("post-definition-expansion", d_assertions);
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// Unconstrained simplification
if(options::unconstrainedSimp()) {
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl;
dumpAssertions("pre-unconstrained-simp", d_assertions);
Chat() << "...doing unconstrained simplification..." << endl;
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
}
unconstrainedSimp();
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl;
dumpAssertions("post-unconstrained-simp", d_assertions);
}
theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl;
dumpAssertions("pre-substitution", d_assertions);
if(options::unsatCores()) {
<< "applying substitutions" << endl;
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
Trace("simplify") << "applying to " << d_assertions[i] << endl;
- spendResource(options::preprocessStep());
+ spendResource(options::preprocessStep());
d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
Trace("simplify") << " got " << d_assertions[i] << endl;
}
}
}
-
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl;
dumpAssertions("post-substitution", d_assertions);
// Assertions ARE guaranteed to be rewritten by this point
}
if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
dumpAssertions("pre-strings-pp", d_assertions);
CVC4::theory::strings::StringsPreprocess sp;
sp.simplify( d_assertions.ref() );
//for (unsigned i = 0; i < d_assertions.size(); ++ i) {
// d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
//}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
dumpAssertions("post-strings-pp", d_assertions);
}
if( d_smt.d_logic.isQuantified() ){
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
//remove rewrite rules
for( unsigned i=0; i < d_assertions.size(); i++ ) {
if( d_assertions[i].getKind() == kind::REWRITE_RULE ){
dumpAssertions("post-skolem-quant", d_assertions);
if( options::macrosQuant() ){
//quantifiers macro expansion
+ quantifiers::QuantifierMacros qm;
bool success;
do{
- quantifiers::QuantifierMacros qm;
success = qm.simplify( d_assertions.ref(), true );
}while( success );
+ //finalize the definitions
+ qm.finalizeDefinitions();
}
//fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
d_smt.d_fmfRecFunctionsConcrete->insert( f, cl );
}
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
}
if( options::sortInference() ){
}
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
dumpAssertions("pre-simplify", d_assertions);
Chat() << "simplifying assertions..." << endl;
noConflict = simplifyAssertions();
if(!noConflict){
++(d_smt.d_stats->d_simplifiedToFalse);
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl;
dumpAssertions("post-simplify", d_assertions);
dumpAssertions("pre-static-learning", d_assertions);
if(options::doStaticLearning()) {
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl;
// Perform static learning
Chat() << "doing static learning..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): "
<< "performing static learning" << endl;
staticLearning();
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << endl;
}
dumpAssertions("post-static-learning", d_assertions);
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl;
dumpAssertions("pre-ite-removal", d_assertions);
{
Chat() << "removing term ITEs..." << endl;
removeITEs();
d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl;
dumpAssertions("post-ite-removal", d_assertions);
dumpAssertions("pre-repeat-simplify", d_assertions);
if(options::repeatSimp()) {
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
Chat() << "re-simplifying assertions..." << endl;
ScopeCounter depth(d_simplifyAssertionsDepth);
noConflict &= simplifyAssertions();
removeITEs();
// Assert(iteRewriteAssertionsEnd == d_assertions.size());
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
}
dumpAssertions("post-repeat-simplify", d_assertions);
Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl;
dumpAssertions("pre-theory-preprocessing", d_assertions);
{
Chat() << "theory preprocessing..." << endl;
d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
}
}
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl;
dumpAssertions("post-theory-preprocessing", d_assertions);
// If we are using eager bit-blasting wrap assertions in fake atom so that
// end: INVARIANT to maintain: no reordering of assertions or
// introducing new ones
+ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
dumpAssertions("post-everything", d_assertions);
//set instantiation level of everything to zero
}
bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
- if( n.getKind()==INST_CONSTANT ){
+ if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
//only legal if current quantified formula contains n
return TermDb::containsTerm( d_curr_quant, n );
}else{
return d_quantEngine->getInstWhenNeedsCheck( e );
}
+unsigned InstantiationEngine::needsModel( Theory::Effort e ) {
+ if( options::cbqiModel() && options::cbqi() ){
+ return QuantifiersEngine::QEFFORT_STANDARD;
+ }else{
+ return QuantifiersEngine::QEFFORT_NONE;
+ }
+}
+
void InstantiationEngine::reset_round( Theory::Effort e ) {
d_cbqi_set_quant_inactive = false;
if( options::cbqi() ){
bool InstantiationEngine::hasNonArithmeticVariable( Node f ){
for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
TypeNode tn = f[0][i].getType();
- if( !tn.isInteger() && !tn.isReal() ){
+ if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
return true;
}
}
void finishInit();
bool needsCheck( Theory::Effort e );
+ unsigned needsModel( Theory::Effort e );
void reset_round( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
bool checkComplete();
#include "theory/rewriter.h"
#include "proof/proof_manager.h"
#include "smt/smt_engine_scope.h"
+#include "theory/quantifiers/modes.h"
+#include "theory/quantifiers/options.h"
using namespace CVC4;
using namespace std;
bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
- Trace("macros") << "Find macros..." << std::endl;
- //first, collect macro definitions
- for( size_t i=0; i<assertions.size(); i++ ){
- processAssertion( assertions[i] );
- }
- bool retVal = false;
- if( doRewrite && !d_macro_defs.empty() ){
- //now, rewrite based on macro definitions
- for( size_t i=0; i<assertions.size(); i++ ){
- Node curr = simplify( assertions[i] );
- if( curr!=assertions[i] ){
+ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_GROUND ? 1 : 2;
+ for( unsigned r=0; r<rmax; r++ ){
+ d_ground_macros = (r==0);
+ Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
+ //first, collect macro definitions
+ std::map< unsigned, Node > simp_assertions;
+ int last_macro = -1;
+ for( int i=0; i<(int)assertions.size(); i++ ){
+ Trace("macros-debug") << " process assertion " << assertions[i] << std::endl;
+ Node curr = assertions[i];
+ //do simplification before process
+ if( doRewrite && !d_macro_defs_new.empty() ){
+ curr = simplify( assertions[i] );
curr = Rewriter::rewrite( curr );
- Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
- PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
- assertions[i] = curr;
- retVal = true;
+ if( curr!=assertions[i] ){
+ simp_assertions[i] = curr;
+ }
+ }
+ if( processAssertion( curr ) ){
+ last_macro = i;
+ //process this assertion again
+ i--;
}
}
- //also store as defined functions
- for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
- Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
- Trace("macros-def") << " basis is : ";
- std::vector< Node > nargs;
- std::vector< Expr > args;
- for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
- Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
- Trace("macros-def") << d_macro_basis[it->first][i] << " ";
- nargs.push_back( bv );
- args.push_back( bv.toExpr() );
+ Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl;
+ if( doRewrite && !d_macro_defs_new.empty() ){
+ bool retVal = false;
+ Trace("macros") << "Do simplifications..." << std::endl;
+ //now, rewrite based on macro definitions
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ Node curr = assertions[i];
+ std::map< unsigned, Node >::iterator it = simp_assertions.find( i );
+ if( it!=simp_assertions.end() ){
+ curr = it->second;
+ }
+ //simplify again if before last macro
+ if( (int)i<last_macro ){
+ curr = simplify( curr );
+ }
+ if( curr!=assertions[i] ){
+ curr = Rewriter::rewrite( curr );
+ Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
+ PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+ assertions[i] = curr;
+ retVal = true;
+ }
}
- Trace("macros-def") << std::endl;
- Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
- smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+ d_macro_defs_new.clear();
+ if( retVal ){
+ return true;
+ }
+ }
+ }
+ for( int i=0; i<(int)assertions.size(); i++ ){
+ if( Trace.isOn("macros-warn") ){
+ debugMacroDefinition( assertions[i], assertions[i] );
}
}
- return retVal;
+ return false;
}
-void QuantifierMacros::processAssertion( Node n ) {
+bool QuantifierMacros::processAssertion( Node n ) {
if( n.getKind()==AND ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- processAssertion( n[i] );
+ if( processAssertion( n[i] ) ){
+ return true;
+ }
}
+ return false;
}else if( n.getKind()==FORALL ){
std::vector< Node > args;
for( size_t j=0; j<n[0].getNumChildren(); j++ ){
args.push_back( n[0][j] );
}
//look at the body of the quantifier for macro definition
- process( n[1], true, args, n );
+ return process( n[1], true, args, n );
+ }else{
+ return false;
}
}
}
}
-bool QuantifierMacros::containsBadOp( Node n, Node op ){
+bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc ){
if( n.getKind()==APPLY_UF ){
Node nop = n.getOperator();
if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){
return true;
}
+ if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
+ opc.push_back( nop );
+ }
+ }else if( d_ground_macros && n.getKind()==FORALL ){
+ return true;
}
for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( containsBadOp( n[i], op ) ){
+ if( containsBadOp( n[i], op, opc ) ){
return true;
}
}
if( n.getNumChildren()==2 && n[0].isConst() ){
getMacroCandidates( n[1], candidates );
}
+ }else if( n.getKind()==NOT ){
+ getMacroCandidates( n[0], candidates );
}
}
//return the opposite side of the equality if defined that way
for( int i=0; i<2; i++ ){
if( lit[i]==n ){
- return lit[ i==0 ? 1 : 0];
+ return lit[i==0 ? 1 : 0];
+ }else if( lit[i].getKind()==NOT && lit[i][0]==n ){
+ return lit[i==0 ? 1 : 0].negate();
}
}
//must solve for term n in the literal lit
return success;
}
-void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
+bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
+ Trace("macros-debug") << " process " << n << std::endl;
if( n.getKind()==NOT ){
- process( n[0], !pol, args, f );
+ return process( n[0], !pol, args, f );
}else if( n.getKind()==AND || n.getKind()==OR ){
//bool favorPol = (n.getKind()==AND)==pol;
//conditional?
}else if( n.getKind()==APPLY_UF ){
//predicate case
if( isBoundVarApplyUf( n ) ){
- Node n_def = NodeManager::currentNM()->mkConst( pol );
- Trace("macros-quant") << "Macro found for " << f << std::endl;
- Trace("macros") << "* " << n_def << " is a macro for " << n.getOperator() << std::endl;
- d_macro_defs[ n.getOperator() ] = n_def;
+ Node op = n.getOperator();
+ if( d_macro_defs.find( op )==d_macro_defs.end() ){
+ Node n_def = NodeManager::currentNM()->mkConst( pol );
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ std::stringstream ss;
+ ss << "mda_" << op << "";
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
+ d_macro_basis[op].push_back( v );
+ }
+ //contains no ops
+ std::vector< Node > op_contains;
+ //add the macro
+ addMacro( op, n_def, op_contains );
+ return true;
+ }
}
}else{
//literal case
getFreeVariables( m, args, fvs, false );
//get definition and condition
Node n_def = solveInEquality( m, n ); //definition for the macro
- //definition must exist and not contain any free variables apart from fvs
- if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op ) ){
+ //definition must exist and not contain any free variables apart from fvs, opc is list of functions it contains
+ std::vector< Node > opc;
+ if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op, opc ) ){
Node n_cond; //condition when this definition holds
//conditional must not contain any free variables apart from fvs
if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){
std::vector< Node > subs;
if( getSubstitution( fvs, solved, vars, subs, true ) ){
n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- Trace("macros-quant") << "Macro found for " << f << std::endl;
- Trace("macros") << "* " << n_def << " is a macro for " << op << std::endl;
- d_macro_defs[op] = n_def;
- return;
+ addMacro( op, n_def, opc );
+ return true;
}
}
}
}
}
}
+ return false;
}
Node QuantifierMacros::simplify( Node n ){
- Trace("macros-debug") << "simplify " << n << std::endl;
- std::vector< Node > children;
- bool childChanged = false;
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- Node nn = simplify( n[i] );
- children.push_back( nn );
- childChanged = childChanged || nn!=n[i];
+ if( n.getNumChildren()==0 ){
+ return n;
+ }else{
+ std::map< Node, Node >::iterator itn = d_simplify_cache.find( n );
+ if( itn!=d_simplify_cache.end() ){
+ return itn->second;
+ }else{
+ Node ret = n;
+ Trace("macros-debug") << " simplify " << n << std::endl;
+ std::vector< Node > children;
+ bool childChanged = false;
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ Node nn = simplify( n[i] );
+ children.push_back( nn );
+ childChanged = childChanged || nn!=n[i];
+ }
+ bool retSet = false;
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
+ std::map< Node, Node >::iterator it = d_macro_defs.find( op );
+ if( it!=d_macro_defs.end() && !it->second.isNull() ){
+ //do substitution if necessary
+ ret = it->second;
+ std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
+ if( itb!=d_macro_basis.end() ){
+ ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+ }
+ retSet = true;
+ }
+ }
+ if( !retSet && childChanged ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ d_simplify_cache[n] = ret;
+ return ret;
+ }
}
+}
+
+void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) {
+ //for debugging, ensure that all previous definitions have been eliminated
if( n.getKind()==APPLY_UF ){
Node op = n.getOperator();
- if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){
- //do substitution if necessary
- std::map< Node, std::vector< Node > >::iterator it = d_macro_basis.find( op );
- Node ret = d_macro_defs[op];
- if( it!=d_macro_basis.end() ){
- ret = ret.substitute( it->second.begin(), it->second.end(), children.begin(), children.end() );
+ if( d_macro_defs.find( op )!=d_macro_defs.end() ){
+ if( d_macro_defs.find( oo )!=d_macro_defs.end() ){
+ Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl;
+ }else{
+ Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl;
}
- return ret;
+ Trace("macros-warn") << " contains defined function " << op << "!!!" << std::endl;
}
}
- if( childChanged ){
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.insert( children.begin(), n.getOperator() );
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ debugMacroDefinition( oo, n[i] );
+ }
+}
+
+void QuantifierMacros::finalizeDefinitions() {
+ if( options::incrementalSolving() || options::produceModels() || Trace.isOn("macros-warn") ){
+ Trace("macros") << "Store as defined functions..." << std::endl;
+ //also store as defined functions
+ for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+ Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
+ Trace("macros-def") << " basis is : ";
+ std::vector< Node > nargs;
+ std::vector< Expr > args;
+ for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
+ Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
+ Trace("macros-def") << d_macro_basis[it->first][i] << " ";
+ nargs.push_back( bv );
+ args.push_back( bv.toExpr() );
+ }
+ Trace("macros-def") << std::endl;
+ Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
+ smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+
+ if( Trace.isOn("macros-warn") ){
+ debugMacroDefinition( it->first, sbody );
+ }
}
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }else{
- return n;
+ Trace("macros") << "done." << std::endl;
}
}
+
+void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
+ Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl;
+ d_simplify_cache.clear();
+ d_macro_defs[op] = n;
+ d_macro_defs_new[op] = n;
+ //substitute into all previous
+ std::vector< Node > dep_ops;
+ dep_ops.push_back( op );
+ Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl;
+ for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){
+ Node cop = d_macro_def_contains[op][i];
+ Node def = d_macro_defs[cop];
+ def = simplify( def );
+ d_macro_defs[cop] = def;
+ if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){
+ d_macro_defs_new[cop] = def;
+ }
+ dep_ops.push_back( cop );
+ }
+ //store the contains op information
+ for( unsigned i=0; i<opc.size(); i++ ){
+ for( unsigned j=0; j<dep_ops.size(); j++ ){
+ Node dop = dep_ops[j];
+ if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){
+ d_macro_def_contains[opc[i]].push_back( dop );
+ }
+ }
+ }
+}
\ No newline at end of file
class QuantifierMacros{
private:
- void processAssertion( Node n );
+ bool d_ground_macros;
+ bool processAssertion( Node n );
bool isBoundVarApplyUf( Node n );
- void process( Node n, bool pol, std::vector< Node >& args, Node f );
+ bool process( Node n, bool pol, std::vector< Node >& args, Node f );
bool contains( Node n, Node n_s );
- bool containsBadOp( Node n, Node op );
+ bool containsBadOp( Node n, Node op, std::vector< Node >& opc );
bool isMacroLiteral( Node n, bool pol );
void getMacroCandidates( Node n, std::vector< Node >& candidates );
Node solveInEquality( Node n, Node lit );
std::map< Node, std::vector< Node > > d_macro_basis;
//map from operators to macro definition
std::map< Node, Node > d_macro_defs;
+ std::map< Node, Node > d_macro_defs_new;
+ //operators to macro ops that contain them
+ std::map< Node, std::vector< Node > > d_macro_def_contains;
+ //simplify cache
+ std::map< Node, Node > d_simplify_cache;
private:
Node simplify( Node n );
+ void addMacro( Node op, Node n, std::vector< Node >& opc );
+ void debugMacroDefinition( Node oo, Node n );
public:
QuantifierMacros(){}
~QuantifierMacros(){}
bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
+ void finalizeDefinitions();
};
}
SYGUS_INV_TEMPL_MODE_POST,
} SygusInvTemplMode;
+typedef enum {
+ /** infer all definitions */
+ MACROS_QUANT_MODE_ALL,
+ /** infer ground definitions */
+ MACROS_QUANT_MODE_GROUND,
+} MacrosQuantMode;
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
# Whether to NNF quantifier bodies
option nnfQuant --nnf-quant bool :default true
apply NNF conversion to quantified formulas
-option clauseSplit --clause-split bool :default false
+option clauseSplit --clause-split bool :default true
apply clause splitting to quantified formulas
# Whether to pre-skolemize quantifier bodies.
# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
# Whether to perform agressive miniscoping
option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
perform aggressive miniscoping for quantifiers
-# Whether to perform quantifier macro expansion
-option macrosQuant --macros-quant bool :default false
- perform quantifiers macro expansions
# Whether to CNF quantifier bodies
option elimTautQuant --elim-taut-quant bool :default true
eliminate tautological disjuncts of quantified formulas
option eMatching --e-matching bool :read-write :default true
whether to do heuristic E-matching
-
+
option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
which ground terms to consider for instantiation
-# Whether to consider terms in the bodies of quantifiers for matching
option registerQuantBodyTerms --register-quant-body-terms bool :default false
consider ground terms within bodies of quantified formulas for matching
-# Whether to use smart triggers
option smartTriggers --smart-triggers bool :default true
disable smart triggers
-# Whether to use relevent triggers
option relevantTriggers --relevant-triggers bool :default false
prefer triggers that are more relevant based on SInE style analysis
option relationalTriggers --relational-triggers bool :default false
selection mode for triggers
option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h"
policy for handling user-provided patterns for quantifier instantiation
+option incrementTriggers --increment-triggers bool :default true
+ generate additional triggers as needed during search
option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
when to apply instantiation
-
option instMaxLevel --inst-max-level=N int :read-write :default -1
maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
option instLevelInputOnly --inst-level-input-only bool :default true
option internalReps --quant-internal-reps bool :default true
instantiate with representatives chosen by quantifiers engine
-option incrementTriggers --increment-triggers bool :default true
- generate additional triggers as needed during search
option eagerInstQuant --eager-inst-quant bool :default false
apply quantifier instantiation eagerly
option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
policy for instantiating axioms
-
### finite model finding options
option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
turns on recursive counterexample-based quantifier instantiation
option cbqiSat --cbqi-sat bool :read-write :default true
answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
+option cbqiModel --cbqi-model bool :read-write :default true
+ guide instantiations by model values for counterexample-based quantifier instantiation
### local theory extensions options
option quantAlphaEquiv --quant-alpha-equiv bool :default true
infer alpha equivalence between quantified formulas
+option macrosQuant --macros-quant bool :default false
+ perform quantifiers macro expansion
+option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h"
+ mode for quantifiers macro expansion
### recursive function options
#option funDefs --fun-defs bool :default false
# enable specialized techniques for recursive function definitions
+### e-unification options
+
+option quantEqualityEngine --quant-ee bool :default false
+ maintain congrunce closure over universal equalities
+
endmodule
+ Synthesize invariant based on strengthening of postcondition. \n\
\n\
";
+static const std::string macrosQuantHelp = "\
+Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
+\n\
+all \n\
++ Infer definitions for functions, including those containing quantified formulas.\n\
+\n\
+ground (default) \n\
++ Only infer ground definitions for functions.\n\
+\n\
+";
inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "pre-full") {
}
}
+inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "all" ) {
+ return MACROS_QUANT_MODE_ALL;
+ } else if(optarg == "ground") {
+ return MACROS_QUANT_MODE_GROUND;
+ } else if(optarg == "help") {
+ puts(macrosQuantHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
+ optarg + "'. Try --macros-quant-mode help.");
+ }
+}
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file quant_equality_engine.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** Congruence closure with free variables
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/quant_equality_engine.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+QuantEqualityEngine::QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ),
+d_notify( *this ),
+d_uequalityEngine(d_notify, c, "theory::quantifiers::QuantEqualityEngine", true),
+d_conflict(c, false),
+d_quant_red(c),
+d_quant_unproc(c){
+ d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
+}
+
+void QuantEqualityEngine::conflict(TNode t1, TNode t2) {
+ //report conflict through quantifiers engine output channel
+ std::vector<TNode> assumptions;
+ d_uequalityEngine.explainEquality(t1, t2, true, assumptions, NULL);
+ Node conflict;
+ if( assumptions.size()==1 ){
+ conflict = assumptions[0];
+ }else{
+ conflict = NodeManager::currentNM()->mkNode( AND, assumptions );
+ }
+ d_conflict = true;
+ Trace("qee-conflict") << "Quantifier equality engine conflict : " << conflict << std::endl;
+ d_quantEngine->getOutputChannel().conflict( conflict );
+}
+
+void QuantEqualityEngine::eqNotifyNewClass(TNode t){
+
+}
+void QuantEqualityEngine::eqNotifyPreMerge(TNode t1, TNode t2){
+
+}
+void QuantEqualityEngine::eqNotifyPostMerge(TNode t1, TNode t2){
+
+}
+void QuantEqualityEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+
+}
+
+/* whether this module needs to check this round */
+bool QuantEqualityEngine::needsCheck( Theory::Effort e ) {
+ return e>=Theory::EFFORT_LAST_CALL;
+}
+
+/* reset at a round */
+void QuantEqualityEngine::reset_round( Theory::Effort e ){
+ //TODO
+}
+
+/* Call during quantifier engine's check */
+void QuantEqualityEngine::check( Theory::Effort e, unsigned quant_e ) {
+ //TODO
+}
+
+/* Called for new quantifiers */
+void QuantEqualityEngine::registerQuantifier( Node q ) {
+ //TODO
+}
+
+/** called for everything that gets asserted */
+void QuantEqualityEngine::assertNode( Node n ) {
+ Assert( n.getKind()==FORALL );
+ Trace("qee-debug") << "QEE assert : " << n << std::endl;
+ Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
+ bool pol = n[1].getKind()!=NOT;
+ if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
+ lit = getTermDatabase()->getCanonicalTerm( lit );
+ Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl;
+ Node t1 = lit.getKind()==APPLY_UF ? lit : lit[0];
+ Node t2;
+ if( lit.getKind()==APPLY_UF ){
+ t2 = pol ? getTermDatabase()->d_true : getTermDatabase()->d_false;
+ pol = true;
+ }else{
+ t2 = lit[1];
+ }
+ bool alreadyHolds = false;
+ if( pol && areUnivEqual( t1, t2 ) ){
+ alreadyHolds = true;
+ }else if( !pol && areUnivDisequal( t1, t2 ) ){
+ alreadyHolds = true;
+ }
+
+ if( alreadyHolds ){
+ d_quant_red.push_back( n );
+ Trace("qee-debug") << "...add to redundant" << std::endl;
+ }else{
+ if( lit.getKind()==APPLY_UF ){
+ d_uequalityEngine.assertPredicate(lit, pol, n);
+ }else{
+ d_uequalityEngine.assertEquality(lit, pol, n);
+ }
+ }
+ }else{
+ d_quant_unproc[n] = true;
+ Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
+ }
+}
+
+bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
+ return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
+}
+
+bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
+ return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
+}
+
+TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
+ if( d_uequalityEngine.hasTerm( n ) ){
+ return d_uequalityEngine.getRepresentative( n );
+ }else{
+ return n;
+ }
+}
\ No newline at end of file
--- /dev/null
+/********************* */
+/*! \file quant_equality_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Congruence closure with free variables
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
+#define __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantEqualityEngine : public QuantifiersModule {
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+private:
+ //notification class for equality engine
+ class NotifyClass : public eq::EqualityEngineNotify {
+ QuantEqualityEngine& d_qee;
+ public:
+ NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {}
+ bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
+ bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_qee.conflict(t1, t2); }
+ void eqNotifyNewClass(TNode t) { d_qee.eqNotifyNewClass(t); }
+ void eqNotifyPreMerge(TNode t1, TNode t2) { d_qee.eqNotifyPreMerge(t1, t2); }
+ void eqNotifyPostMerge(TNode t1, TNode t2) { d_qee.eqNotifyPostMerge(t1, t2); }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_qee.eqNotifyDisequal(t1, t2, reason); }
+ };/* class ConjectureGenerator::NotifyClass */
+ /** The notify class */
+ NotifyClass d_notify;
+ /** (universal) equaltity engine */
+ eq::EqualityEngine d_uequalityEngine;
+ /** Are we in conflict */
+ context::CDO<bool> d_conflict;
+ /** list of redundant quantifiers in current context */
+ context::CDList<Node> d_quant_red;
+ /** unprocessed quantifiers in current context */
+ NodeBoolMap d_quant_unproc;
+private:
+ void conflict(TNode t1, TNode t2);
+ void eqNotifyNewClass(TNode t);
+ void eqNotifyPreMerge(TNode t1, TNode t2);
+ void eqNotifyPostMerge(TNode t1, TNode t2);
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+public:
+ QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
+ ~QuantEqualityEngine(){}
+
+ /* whether this module needs to check this round */
+ bool needsCheck( Theory::Effort e );
+ /* reset at a round */
+ void reset_round( Theory::Effort e );
+ /* Call during quantifier engine's check */
+ void check( Theory::Effort e, unsigned quant_e );
+ /* Called for new quantifiers */
+ void registerQuantifier( Node q );
+ /** called for everything that gets asserted */
+ void assertNode( Node n );
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const { return "QuantEqualityEngine"; }
+ /** queries */
+ bool areUnivDisequal( TNode n1, TNode n2 );
+ bool areUnivEqual( TNode n1, TNode n2 );
+ TNode getUnivRepresentative( TNode n );
+};
+
+
+}
+}
+}
+
+#endif
std::map< Node, bool > activeMap;
computeArgs( args, activeMap, n );
for( unsigned i=0; i<args.size(); i++ ){
- if( activeMap[args[i]] ){
+ if( activeMap.find( args[i] )!=activeMap.end() ){
activeArgs.push_back( args[i] );
}
}
Assert( activeArgs.empty() );
std::map< Node, bool > activeMap;
computeArgs( args, activeMap, n );
- computeArgs( args, activeMap, ipl );
- for( unsigned i=0; i<args.size(); i++ ){
- if( activeMap[args[i]] ){
- activeArgs.push_back( args[i] );
+ if( !activeMap.empty() ){
+ //collect variables in inst pattern list only if we cannot eliminate quantifier
+ computeArgs( args, activeMap, ipl );
+ for( unsigned i=0; i<args.size(); i++ ){
+ if( activeMap.find( args[i] )!=activeMap.end() ){
+ activeArgs.push_back( args[i] );
+ }
}
}
}
}
-void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
+void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
std::vector< Node >& conj ){
if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
std::vector< Node > children;
children.push_back( n );
std::vector< Node > vars;
- //add all positive testers
+ //add all positive testers
for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){
children.push_back( it->second.negate() );
vars.push_back( it->first );
}
return body;
}
-
+
Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) {
if( body.getKind()==OR ){
size_t var_found_count = 0;
Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
std::vector< Node > activeArgs;
- //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
+ //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
if( options::ceGuidedInst() && !ipl.isNull() ){
for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl;
}
bool TermDb::isComm( Kind k ) {
- return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+ return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
}
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/ambqi_builder.h"
#include "theory/quantifiers/fun_def_engine.h"
+#include "theory/quantifiers/quant_equality_engine.h"
using namespace std;
using namespace CVC4;
if( !options::finiteModelFind() || options::fmfInstEngine() ){
d_inst_engine = new quantifiers::InstantiationEngine( this );
d_modules.push_back( d_inst_engine );
+ if( options::cbqi() && options::cbqiModel() ){
+ needsBuilder = true;
+ }
}else{
d_inst_engine = NULL;
}
//}else{
d_fun_def_engine = NULL;
//}
+ if( options::quantEqualityEngine() ){
+ d_uee = new quantifiers::QuantEqualityEngine( this, c );
+ d_modules.push_back( d_uee );
+ }else{
+ d_uee = NULL;
+ }
+
if( needsBuilder ){
Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
delete d_ceg_inst;
delete d_lte_part_inst;
delete d_fun_def_engine;
+ delete d_uee;
for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
delete (*i).second;
}
if( d_hasAddedLemma ){
break;
//otherwise, complete the model generation if necessary
- }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() ){
+ }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() && e==Theory::EFFORT_LAST_CALL ){
Trace("quant-engine-debug") << "Build completed model..." << std::endl;
d_builder->buildModel( d_model, true );
}
std::map< Node, bool >::iterator it = d_quants_red.find( q );
if( it==d_quants_red.end() ){
if( d_alpha_equiv ){
- Trace("quant-engine-debug") << "Alpha equivalence " << q << "?" << std::endl;
+ Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
//add equivalence with another quantified formula
if( !d_alpha_equiv->registerQuantifier( q ) ){
- Trace("quant-engine-debug") << "...alpha equivalence success." << std::endl;
+ Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
++(d_statistics.d_red_alpha_equiv);
d_quants_red[q] = true;
return true;
}
if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){
//will partially instantiate
- Trace("quant-engine-debug") << "LTE: Partially instantiate " << q << "?" << std::endl;
+ Trace("quant-engine-red") << "LTE: Partially instantiate " << q << "?" << std::endl;
if( d_lte_part_inst->addQuantifier( q ) ){
- Trace("quant-engine-debug") << "...LTE partially instantiate success." << std::endl;
+ Trace("quant-engine-red") << "...LTE partially instantiate success." << std::endl;
//delayed reduction : assert to model
d_model->assertQuantifier( q, true );
++(d_statistics.d_red_lte_partial_inst);
//d_curr_out->lemma( lem, false, true );
d_lemmas_produced_c[ lem ] = true;
d_lemmas_waiting.push_back( lem );
- Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl;
+ Trace("inst-add-debug2") << "Added lemma" << std::endl;
return true;
}else{
Trace("inst-add-debug2") << "Duplicate." << std::endl;
}
void QuantifiersEngine::printInstantiations( std::ostream& out ) {
+ bool printed = false;
for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
+ printed = true;
out << "Skolem constants of " << it->first << " : " << std::endl;
out << " ( ";
for( unsigned i=0; i<d_term_db->d_skolem_constants[it->first].size(); i++ ){
}
if( options::incrementalSolving() ){
for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+ printed = true;
out << "Instantiations of " << it->first << " : " << std::endl;
it->second->print( out, it->first );
}
}else{
for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
+ printed = true;
out << "Instantiations of " << it->first << " : " << std::endl;
it->second.print( out, it->first );
out << std::endl;
}
}
+ if( !printed ){
+ out << "No instantiations." << std::endl;
+ }
}
void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
class LtePartialInst;
class AlphaEquivalence;
class FunDefEngine;
+ class QuantEqualityEngine;
}/* CVC4::theory::quantifiers */
namespace inst {
quantifiers::LtePartialInst * d_lte_part_inst;
/** function definitions engine */
quantifiers::FunDefEngine * d_fun_def_engine;
+ /** quantifiers equality engine */
+ quantifiers::QuantEqualityEngine * d_uee;
public: //effort levels
enum {
QEFFORT_CONFLICT,
quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
/** function definition engine */
quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
+ /** quantifiers equality engine */
+ quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
private:
/** owner of quantified formulas */
std::map< Node, QuantifiersModule * > d_owner;
simp-len.smt2 \
is-even.smt2 \
is-even-pred.smt2 \
- delta-simp.smt2
+ delta-simp.smt2 \
+ nested-delta.smt2 \
+ nested-inf.smt2
+
+
# regression can be solved with --finite-model-find --fmf-inst-engine
# set3.smt2
--- /dev/null
+; COMMAND-LINE: --cbqi-recurse
+; EXPECT: sat
+(set-logic LRA)
+(set-info :status sat)
+(assert (forall ((x Real)) (or (exists ((y Real)) (and (< y 0) (< y x))) (<= x 0))))
+(check-sat)
\ No newline at end of file
--- /dev/null
+; COMMAND-LINE: --cbqi-recurse
+; EXPECT: sat
+(set-logic LRA)
+(set-info :status sat)
+(assert (forall ((x Real)) (exists ((y Real)) (> y x))))
+(check-sat)
\ No newline at end of file
projects / cvc5.git / commitdiff