From aeb5013fda3a20f90859541139930c5efb775fe6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Oct 2018 12:15:40 -0500 Subject: [PATCH] Fix cache for sygus post-condition inference (#2592) --- .../sygus/ce_guided_single_inv.cpp | 16 +++++-- .../quantifiers/sygus/ce_guided_single_inv.h | 46 ++++++++++++++++++- test/regress/CMakeLists.txt | 1 + test/regress/Makefile.tests | 1 + .../regress1/sygus/inv-missed-sol-true.sy | 25 ++++++++++ 5 files changed, 82 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress1/sygus/inv-missed-sol-true.sy diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 36690cfcc..b698422a7 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -804,7 +804,7 @@ void TransitionInference::process( Node n ) { } for( unsigned i=0; i visited; + std::map > visited; std::map< bool, Node > terms; std::vector< Node > disjuncts; Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn << std::endl; @@ -949,10 +949,16 @@ void TransitionInference::getNormalizedSubstitution( } } -bool TransitionInference::processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, - std::map< Node, bool >& visited, bool topLevel ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; +bool TransitionInference::processDisjunct( + Node n, + std::map& terms, + std::vector& disjuncts, + std::map >& visited, + bool topLevel) +{ + if (visited[topLevel].find(n) == visited[topLevel].end()) + { + visited[topLevel][n] = true; bool childTopLevel = n.getKind()==OR && topLevel; //if another part mentions UF or a free variable, then fail bool lit_pol = n.getKind()!=NOT; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index c797bc3cb..cfd7cd23b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -58,9 +58,47 @@ public: void print( const char* c ); }; +/** + * This class is used for inferring that an arbitrary synthesis conjecture + * corresponds to an invariant synthesis problem for some predicate (d_func). + * + * The invariant-to-synthesize can either be explicitly given, via a call + * to initialize( f, vars ), or otherwise inferred if this method is not called. + */ class TransitionInference { -private: - bool processDisjunct( Node n, std::map< bool, Node >& terms, std::vector< Node >& disjuncts, std::map< Node, bool >& visited, bool topLevel ); + private: + /** process disjunct + * + * The purpose of this function is to infer pre/post/transition conditions + * for a (possibly unknown) invariant-to-synthesis, given a conjunct from + * an arbitrary synthesis conjecture. + * + * Assume our negated synthesis conjecture is of the form: + * forall f. exists x. (and (or F11 ... F1{m_1}) ... (or Fn1 ... Fn{m_n})) + * This method is called on each (or Fi1 ... Fi{m_i}), where topLevel is true + * for each of Fi1...F1{m_i} and false otherwise. It adds each of Fi1..Fi{m_i} + * to disjuncts. + * + * If this method returns true, then (1) all applications of free function + * symbols have operator d_func. Note this function may set d_func to a + * function symbol in n if d_func was null prior to this call. In other words, + * this method may infer the subject of the invariant synthesis problem; + * (2) all occurrences of d_func are "top-level", that is, each Fij may be + * of the form (not) ( tj ), but otherwise d_func does not occur in + * (or Fi1 ... Fi{m_i}); (3) there exists at most one occurrence of + * ( tj ), and (not ( tk )). + * + * If the above conditions are met, then terms[true] is set to ( tj ) + * if Fij is ( tj ) for some j, and likewise terms[false] + * is set to ( tk ) if Fik is (not ( tk )) for some k. + * + * The argument visited caches the results of this function for (topLevel, n). + */ + bool processDisjunct(Node n, + std::map& terms, + std::vector& disjuncts, + std::map >& visited, + bool topLevel); void getConstantSubstitution( std::vector< Node >& vars, std::vector< Node >& disjuncts, std::vector< Node >& const_var, std::vector< Node >& const_subs, bool reqPol ); bool d_complete; /** get normalized substitution @@ -89,6 +127,10 @@ private: TransitionInference() : d_complete( false ) {} std::vector< Node > d_vars; std::vector< Node > d_prime_vars; + /** + * The function (predicate) that is the subject of the invariant synthesis + * problem we are inferring. + */ Node d_func; class Component { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 441327b3a..19513ada3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1585,6 +1585,7 @@ set(regress_1_tests regress1/sygus/icfp_28_10.sy regress1/sygus/icfp_easy-ite.sy regress1/sygus/inv-example.sy + regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 4e9837c36..5bd187e8f 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1582,6 +1582,7 @@ REG1_TESTS = \ regress1/sygus/icfp_28_10.sy \ regress1/sygus/icfp_easy-ite.sy \ regress1/sygus/inv-example.sy \ + regress1/sygus/inv-missed-sol-true.sy \ regress1/sygus/inv-unused.sy \ regress1/sygus/large-const-simp.sy \ regress1/sygus/let-bug-simp.sy \ diff --git a/test/regress/regress1/sygus/inv-missed-sol-true.sy b/test/regress/regress1/sygus/inv-missed-sol-true.sy new file mode 100644 index 000000000..b04022766 --- /dev/null +++ b/test/regress/regress1/sygus/inv-missed-sol-true.sy @@ -0,0 +1,25 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-inv inv-f ((x Int) (z Int))) + +(declare-primed-var x Int) +(declare-primed-var z Int) + +(define-fun pre-f ((x Int) (z Int)) Bool + (and (> x (- 0 100)) (< x 200) + (> z 100) (< z 200))) + +(define-fun trans-f ((x Int) (z Int) (x! Int) (z! Int)) Bool + (and (< x 100) (> z 100) + (or (and (= x! (+ x 1)) (= z! z)) + (and (= x! (- x 1)) (= z! (- z 1)))))) + +(define-fun post-f ((x Int) (z Int)) Bool + (or (and (< x 100) (> z 100)) + (or (>= x 100) (<= z 100)))) + +(inv-constraint inv-f pre-f trans-f post-f) + +(check-synth) \ No newline at end of file -- 2.30.2