diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-02 08:49:17 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-02 08:49:17 -0600 |
| commit | 2a19474cdb6761fd4c9aeb0165e661c531ba3e38 (patch) | |
| tree | 93847be6dabad4ba94af90a2f63008c66539bd24 /src/theory/quantifiers/sygus/sygus_invariance.cpp | |
| parent | 41b38de8b059d346764cd5ca112740aa09e1d163 (diff) | |
Optimizations for PBE strings (#2728)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_invariance.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.cpp | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 24b47b216..5ea01ef57 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -218,15 +218,22 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre); Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl; Node contr = Rewriter::rewrite(cont); - if (contr == tds->d_false) + if (!contr.isConst()) + { + if (d_isUniversal) + { + return false; + } + } + else if (contr.getConst<bool>() == d_isUniversal) { if (Trace.isOn("sygus-pbe-cterm")) { Trace("sygus-pbe-cterm") << "PBE-cterm : enumerator : do not consider "; - Trace("sygus-pbe-cterm") << nbv << " for any " - << tds->sygusToBuiltin(x) << " since " - << std::endl; + Trace("sygus-pbe-cterm") + << nbv << " for any " << tds->sygusToBuiltin(x) << " since " + << std::endl; Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : "; for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++) { @@ -238,13 +245,13 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, Trace("sygus-pbe-cterm") << " PBE-cterm : and is not in output : " << out << std::endl; } - return true; + return !d_isUniversal; } Trace("sygus-pbe-cterm-debug2") << "...check failed, rewrites to : " << contr << std::endl; } } - return false; + return d_isUniversal; } } /* CVC4::theory::quantifiers namespace */ |