Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.
This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.
After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
options::unconstrainedSimp.set(uncSimp);
}
}
+ if (!options::proof())
+ {
+ // minimizing solutions from single invocation requires proofs
+ if (options::cegqiSolMinCore() && options::cegqiSolMinCore.wasSetByUser())
+ {
+ throw OptionException("cegqi-si-sol-min-core requires --proof");
+ }
+ }
// Disable options incompatible with unsat cores and proofs or output an
// error if enabled explicitly
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "util/random.h"
using namespace CVC4;
//--------------------------------- collecting finite input/output domain information
-void SygusPbe::collectExamples(Node n,
+bool SygusPbe::collectExamples(Node n,
std::map<Node, bool>& visited,
bool hasPol,
bool pol)
{
neval = n;
if( hasPol ){
- n_output = !pol ? d_true : d_false;
+ n_output = pol ? d_true : d_false;
}
neval_is_evalapp = true;
- }else if( n.getKind()==EQUAL && hasPol && !pol ){
+ }
+ else if (n.getKind() == EQUAL && hasPol && pol)
+ {
for( unsigned r=0; r<2; r++ ){
if (n[r].getKind() == DT_SYGUS_EVAL)
{
// is it an evaluation function?
if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
{
+ Trace("sygus-pbe-debug")
+ << "Process head: " << n << " == " << n_output << std::endl;
+ // If n_output is null, then neval does not have a constant value
+ // If n_output is non-null, then neval is constrained to always be
+ // that value.
+ if (!n_output.isNull())
+ {
+ std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
+ if (itet == d_exampleTermMap.end())
+ {
+ d_exampleTermMap[neval] = n_output;
+ }
+ else if (itet->second != n_output)
+ {
+ // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
+ // the conjecture is infeasible.
+ return false;
+ }
+ }
// get the evaluation head
Node eh = neval[0];
std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
Assert(n_output.isConst());
}
// finished processing this node
- return;
+ return true;
}
d_examples_invalid[eh] = true;
d_examples_out_invalid[eh] = true;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
bool newHasPol;
bool newPol;
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- collectExamples( n[i], visited, newHasPol, newPol );
+ QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
+ if (!collectExamples(n[i], visited, newHasPol, newPol))
+ {
+ return false;
+ }
}
}
+ return true;
}
bool SygusPbe::initialize(Node n,
std::vector<Node>& lemmas)
{
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
for (unsigned i = 0; i < candidates.size(); i++)
{
}
std::map<Node, bool> visited;
- collectExamples(n, visited, true, true);
+ // n is negated conjecture
+ if (!collectExamples(n, visited, true, false))
+ {
+ Trace("sygus-pbe") << "...conflicting examples" << std::endl;
+ Node infeasible = d_parent->getGuard().negate();
+ lemmas.push_back(infeasible);
+ return false;
+ }
for (unsigned i = 0; i < candidates.size(); i++)
{
tn_to_strategy_pt[tnsp].push_back(p.first);
}
// initialize the enumerators
- NodeManager* nm = NodeManager::currentNM();
for (const Node& e : d_candidate_to_enum[c])
{
TypeNode etn = e.getType();
* For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
*/
std::map<Node, std::vector<Node> > d_examples_term;
+ /**
+ * Map from example input terms to their output, for example [EX#1] above,
+ * this is { f( 0 ) -> 2, f( 5 ) -> 7, f( 6 ) -> 8 }.
+ */
+ std::map<Node, Node> d_exampleTermMap;
/** collect the PBE examples in n
- * This is called on the input conjecture, and will populate the above vectors.
- * hasPol/pol denote the polarity of n in the conjecture.
- */
- void collectExamples(Node n,
+ * This is called on the input conjecture, and will populate the above
+ * vectors, where hasPol/pol denote the polarity of n in the conjecture. This
+ * function returns false if it finds two examples that are contradictory.
+ */
+ bool collectExamples(Node n,
std::map<Node, bool>& visited,
bool hasPol,
bool pol);
Trace("sygus-sui-enum")
<< " ...fail : term is not unique" << std::endl;
}
- d_cond_count++;
}
if (keep)
{
// notify to retry the build of solution
d_check_sol = true;
+ d_cond_count++;
ecv.addEnumValue(v, results);
}
}
d_quant = q;
NodeManager* nm = NodeManager::currentNM();
+ // initialize the guard
+ d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
+ d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
+ d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
+ AlwaysAssert(!d_feasible_guard.isNull());
+
// pre-simplify the quantified formula based on the process utility
d_simp_quant = d_ceg_proc->preSimplify(d_quant);
}
}
- // initialize the guard
- d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
- d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
- d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
- AlwaysAssert(!d_feasible_guard.isNull());
// register the strategy
d_feasible_strategy.reset(
new DecisionStrategySingleton("sygus_feasible",
regress0/sygus/real-si-all.sy
regress0/sygus/strings-unconstrained.sy
regress0/sygus/uminus_one.sy
+ regress0/sygus/univ_3-long-repeat-conflict.sy
regress0/test11.cvc
regress0/test9.cvc
regress0/tptp/ARI086=1.p
--- /dev/null
+; EXPECT: unknown
+; COMMAND-LINE: --sygus-out=status
+(set-logic SLIA)
+
+(synth-fun f ((col1 String) (col2 String)) String
+ ((Start String (ntString))
+ (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"
+ (str.++ ntString ntString)
+ (str.replace ntString ntString ntString)
+ (str.at ntString ntInt)
+ (int.to.str ntInt)
+ (ite ntBool ntString ntString)
+ (str.substr ntString ntInt ntInt)))
+ (ntInt Int (0 1 2
+ (+ ntInt ntInt)
+ (- ntInt ntInt)
+ (str.len ntString)
+ (str.to.int ntString)
+ (str.indexof ntString ntString ntInt)))
+ (ntBool Bool (true false
+ (str.prefixof ntString ntString)
+ (str.suffixof ntString ntString)
+ (str.contains ntString ntString)))))
+
+
+(declare-var col1 String)
+(declare-var col2 String)
+(constraint (= (f "UC Berkeley" "Berkeley, CA")
+ "Berkeley, CA, USA"))
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")
+ "Phialdelphia, PA, USA"))
+(constraint (= (f "UCLA" "Los Angeles, CA")
+ "UCLA, Los Angeles, CA, USA"))
+(constraint (= (f "Cornell University" "Ithaca, New York, USA")
+ "Ithaca, New York, USA"))
+(constraint (= (f "Penn" "Philadelphia, PA, USA")
+ "Philadelphia, PA, USA"))
+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")
+ "Ann Arbor, MI, USA"))
+(constraint (= (f "UC Berkeley" "Berkeley, CA")
+ "Berkeley, CA, USA"))
+(constraint (= (f "MIT" "Cambridge, MA")
+ "Cambridge, MA, USA"))
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")
+ "Phialdelphia, PA, USA"))
+(constraint (= (f "UCLA" "Los Angeles, CA")
+ "Los Angeles, CA, USA"))
+
+; has contradictory examples
+(check-synth)
+; REQUIRES: proof
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof
(set-logic LIA)
(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
(declare-var x1 Int)
projects / cvc5.git / commitdiff