diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-04 17:48:30 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-04 17:48:30 -0600 |
commit | 2a888bdb47b18ea29f67659b5d64aad6d8da389b (patch) | |
tree | 6cad86505a6d357e96b16d57c5b4ef4ebd5c411a /src/theory | |
parent | e5ac2503afc1879808a8809e9b9498ba08217328 (diff) |
Make check synth solution robust to auxiliary assertions (#3432)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 3 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 |
8 files changed, 19 insertions, 12 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index d8c69edac..5edd18464 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1144,7 +1144,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out) } } -bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map) +bool SynthConjecture::getSynthSolutions( + std::map<Node, std::map<Node, Node> >& sol_map) { NodeManager* nm = NodeManager::currentNM(); std::vector<Node> sols; @@ -1153,6 +1154,8 @@ bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map) { return false; } + // we add it to the solution map, indexed by this conjecture + std::map<Node, Node>& smc = sol_map[d_quant]; for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node sol = sols[i]; @@ -1182,7 +1185,7 @@ bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map) Assert(fvar.getType().isComparableTo(bsol.getType())); } // store in map - sol_map[fvar] = bsol; + smc[fvar] = bsol; } return true; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index a86ff6f75..344f8b460 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -116,13 +116,14 @@ class SynthConjecture * This method returns true if this class has a solution available to the * conjecture that it was assigned. * - * This method adds entries to sol_map that map functions-to-synthesize to + * Let q be the synthesis conjecture assigned to this class. + * This method adds entries to sol_map[q] that map functions-to-synthesize to * their builtin solution, which has the same type. For example, for synthesis - * conjecture exists f. forall x. f( x )>x, this function may return the map - * containing the entry: + * conjecture exists f. forall x. f( x )>x, this function will update + * sol_map[q] to contain the entry: * f -> (lambda x. x+1) */ - bool getSynthSolutions(std::map<Node, Node>& sol_map); + bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map); /** * The feasible guard whose semantics are "this conjecture is feasiable". * This is "G" in Figure 3 of Reynolds et al CAV 2015. diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 73105af6f..88d00ce3a 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -387,7 +387,8 @@ void SynthEngine::printSynthSolution(std::ostream& out) } } -bool SynthEngine::getSynthSolutions(std::map<Node, Node>& sol_map) +bool SynthEngine::getSynthSolutions( + std::map<Node, std::map<Node, Node> >& sol_map) { bool ret = true; for (unsigned i = 0, size = d_conjs.size(); i < size; i++) diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index b5880b0c1..20e4deec6 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -88,7 +88,7 @@ class SynthEngine : public QuantifiersModule * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - bool getSynthSolutions(std::map<Node, Node>& sol_map); + bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map); /** preregister assertion (before rewrite) * * The purpose of this method is to inform the solution reconstruction diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index dfda79aec..8337ba0b0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1294,7 +1294,8 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ return ret; } -bool QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map) +bool QuantifiersEngine::getSynthSolutions( + std::map<Node, std::map<Node, Node> >& sol_map) { return d_private->d_synth_e->getSynthSolutions(sol_map); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f84b59761..d1d7f1633 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -268,7 +268,7 @@ public: * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - bool getSynthSolutions(std::map<Node, Node>& sol_map); + bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map); //----------end user interface for instantiations diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d73babdc0..7a72367de 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -944,7 +944,8 @@ TheoryModel* TheoryEngine::getBuiltModel() return d_curr_model; } -bool TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map) +bool TheoryEngine::getSynthSolutions( + std::map<Node, std::map<Node, Node>>& sol_map) { if (d_quantEngine) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index fc31572ec..dd34ae16b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -779,7 +779,7 @@ public: * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - bool getSynthSolutions(std::map<Node, Node>& sol_map); + bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map); /** * Get the model builder |