summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp8
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp22
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.h4
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp4
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.h4
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv_sol.cpp59
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv_sol.h7
-rw-r--r--src/theory/quantifiers/options2
8 files changed, 104 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 498b2ee12..1a9887e93 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -85,6 +85,7 @@
#include "theory/quantifiers/macros.h"
#include "theory/quantifiers/fun_def_process.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/options.h"
#include "theory/datatypes/options.h"
#include "theory/strings/theory_strings_preprocess.h"
@@ -3170,6 +3171,13 @@ void SmtEnginePrivate::processAssertions() {
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
+ if( options::ceGuidedInst() ){
+ //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] );
+ }
+ }
+
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
!d_smt.d_logic.isPure(THEORY_BV)) {
throw ModalException("Eager bit-blasting does not currently support theory combination. "
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f01efb5c4..0bc5bb008 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -150,6 +150,10 @@ bool CegConjecture::needsCheck() {
return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
}
+void CegConjecture::preregisterConjecture( Node q ) {
+ d_ceg_si->preregisterConjecture( q );
+}
+
CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
d_conj = new CegConjecture( qe, qe->getSatContext() );
d_last_inst_si = false;
@@ -592,6 +596,24 @@ void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
}
}
+void CegInstantiation::preregisterAssertion( Node n ) {
+ //check if it sygus conjecture
+ if( n.getKind()==FORALL ){
+ if( n.getNumChildren()==3 ){
+ for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
+ if( n[2][i].getKind()==INST_ATTRIBUTE ){
+ Node avar = n[2][i][0];
+ if( avar.getAttribute(SygusAttribute()) ){
+ //this is a sygus conjecture
+ Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
+ d_conj->preregisterConjecture( n );
+ }
+ }
+ }
+ }
+ }
+}
+
CegInstantiation::Statistics::Statistics():
d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 9228f11b6..8aa2e2c26 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -89,6 +89,8 @@ public: //for fairness
bool isSingleInvocation();
/** needs check */
bool needsCheck();
+ /** preregister conjecture */
+ void preregisterConjecture( Node q );
};
@@ -139,6 +141,8 @@ public:
void printSynthSolution( std::ostream& out );
/** collect disjuncts */
static void collectDisjuncts( Node n, std::vector< Node >& ex );
+ /** preregister assertion (before rewrite) */
+ void preregisterAssertion( Node n );
public:
class Statistics {
public:
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index c31ebd9ab..19cf9b008 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -806,6 +806,7 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
//reconstruct the solution into sygus if necessary
reconstructed = 0;
if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() ){
+ d_sol->preregisterConjecture( d_orig_conjecture );
d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed );
if( reconstructed==1 ){
Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
@@ -859,5 +860,8 @@ bool CegConjectureSingleInv::needsCheck() {
return true;
}
+void CegConjectureSingleInv::preregisterConjecture( Node q ) {
+ d_orig_conjecture = q;
+}
} \ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 8950b2642..e814df110 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -84,6 +84,8 @@ private:
//lemmas produced
inst::InstMatchTrie d_inst_match_trie;
inst::CDInstMatchTrie * d_c_inst_match_trie;
+ //original conjecture
+ Node d_orig_conjecture;
// solution
std::vector< Node > d_varList;
Node d_orig_solution;
@@ -129,6 +131,8 @@ public:
bool isSingleInvocation() { return !d_single_inv.isNull(); }
//needs check
bool needsCheck();
+ /** preregister conjecture */
+ void preregisterConjecture( Node q );
};
}
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 413fd9ba2..bac39f22c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -618,9 +618,27 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
}
-
-
-
+void CegConjectureSingleInvSol::preregisterConjecture( Node q ) {
+ Trace("csi-sol") << "Preregister conjecture : " << q << std::endl;
+ Node n = q;
+ if( n.getKind()==FORALL ){
+ n = n[1];
+ }
+ if( n.getKind()==EXISTS ){
+ if( n[0].getNumChildren()==d_varList.size() ){
+ std::vector< Node > evars;
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ evars.push_back( n[0][i] );
+ }
+ n = n[1].substitute( evars.begin(), evars.end(), d_varList.begin(), d_varList.end() );
+ }else{
+ Trace("csi-sol") << "Not the same number of variables, return." << std::endl;
+ return;
+ }
+ }
+ Trace("csi-sol") << "Preregister node for solution reconstruction : " << n << std::endl;
+ registerEquivalentTerms( n );
+}
Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed ) {
Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
@@ -1108,7 +1126,38 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector<
nn = Rewriter::rewrite( nn );
equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
}
- }
-}
+ }
+ //based on eqt cache
+ std::map< Node, Node >::iterator itet = d_eqt_rep.find( n );
+ if( itet!=d_eqt_rep.end() ){
+ Node rn = itet->second;
+ for( unsigned i=0; i<d_eqt_eqc[rn].size(); i++ ){
+ if( d_eqt_eqc[rn][i]!=n ){
+ if( std::find( equiv.begin(), equiv.end(), d_eqt_eqc[rn][i] )==equiv.end() ){
+ equiv.push_back( d_eqt_eqc[rn][i] );
+ }
+ }
+ }
+ }
+}
+
+void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) {
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ registerEquivalentTerms( n[i] );
+ }
+ Node rn = Rewriter::rewrite( n );
+ if( rn!=n ){
+ Trace("csi-equiv") << " eq terms : " << n << " " << rn << std::endl;
+ d_eqt_rep[n] = rn;
+ d_eqt_rep[rn] = rn;
+ if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), rn )==d_eqt_eqc[rn].end() ){
+ d_eqt_eqc[rn].push_back( rn );
+ }
+ if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), n )==d_eqt_eqc[rn].end() ){
+ d_eqt_eqc[rn].push_back( n );
+ }
+ }
+}
+
}
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 1d84986b4..adcc7bf85 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -65,6 +65,10 @@ private:
std::map< int, std::vector< int > > d_eqc;
std::map< int, int > d_rep;
+
+ //equivalent terms
+ std::map< Node, Node > d_eqt_rep;
+ std::map< Node, std::vector< Node > > d_eqt_eqc;
//cache when reconstructing solutions
std::vector< int > d_tmp_fail;
@@ -80,8 +84,11 @@ private:
void setReconstructed( int id, Node n );
//get equivalent terms to n with top symbol k
void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
+ //register equivalent terms
+ void registerEquivalentTerms( Node n );
public:
Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
+ void preregisterConjecture( Node q );
public:
CegConjectureSingleInvSol( QuantifiersEngine * qe );
};
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index ec71e5348..753f3f170 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -226,7 +226,7 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
generalize based on content in global search space narrowing
-option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
+option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
template mode for sygus invariant synthesis
# approach applied to general quantified formulas
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback