diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-18 00:04:26 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-18 00:04:26 +0200 |
| commit | 1aaf70f23d8f2061e5c05ca98d12deea06494a25 (patch) | |
| tree | 5e8d5c889930cfe368c26c0211a8d3c4ed162004 /src/theory | |
| parent | 548582b252170f35a602705a109d88a608611cca (diff) | |
Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quantified formulas with non-constant polarity.
Diffstat (limited to 'src/theory')
| -rwxr-xr-x | src/theory/quantifiers/alpha_equivalence.cpp | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 5 |
2 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 84bf2ec14..b72f15a01 100755 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -55,9 +55,9 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE return true; }else{ //lemma ( q <=> d_quant ) - Trace("alpha-eq") << "Alpha equivalent : " << std::endl; - Trace("alpha-eq") << " " << q << std::endl; - Trace("alpha-eq") << " " << aen->d_quant << std::endl; + Trace("quant-ae") << "Alpha equivalent : " << std::endl; + Trace("quant-ae") << " " << q << std::endl; + Trace("quant-ae") << " " << aen->d_quant << std::endl; qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); return false; } diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 632e19a18..7d5e33fdb 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -119,6 +119,11 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl; if( n.getKind()==FORALL ){ Node c = simplifyFormula( n[1], pol, hasPol, constraints, hd, is_fun_def ); + //append prenex to constraints + for( unsigned i=0; i<constraints.size(); i++ ){ + constraints[i] = NodeManager::currentNM()->mkNode( FORALL, n[0], constraints[i] ); + constraints[i] = Rewriter::rewrite( constraints[i] ); + } if( c!=n[1] ){ return NodeManager::currentNM()->mkNode( FORALL, n[0], c ); }else{ |