Parser improvement

CMakeLists.txt

@@ -5,8 +5,8 @@ cmake_policy(SET CMP0074 NEW)
 endif()
 
 set(OPENSMT_VERSION_MAJOR 2)
-set(OPENSMT_VERSION_MINOR 4)
-set(OPENSMT_VERSION_PATCH 3)
+set(OPENSMT_VERSION_MINOR 5)
+set(OPENSMT_VERSION_PATCH 0)
 set(OPENSMT_VERSION ${OPENSMT_VERSION_MAJOR}.${OPENSMT_VERSION_MINOR}.${OPENSMT_VERSION_PATCH})
 project(opensmt VERSION ${OPENSMT_VERSION} LANGUAGES CXX)
 

Changelog.md

@@ -1,6 +1,14 @@
-### 2.4.3 (unreleased)
+### 2.5.0 (unreleased)
 
 
+
+### 2.4.3 (2022-11-21)
+
+Bug fixes:
+ - UFLA: Fix unsoundness bug due to LASolver not signalling the presence of conflict correctly
+ - ArithLogic: Fix substitution computation in the presence of uninterpreted functions
+ - Logic: Evaluate `distinct` function on constant arguments (required for model evaluation)
+
 ### 2.4.2 (2022-10-24)
 
 Bug fixes:

benchmark/CMakeLists.txt

@@ -3,7 +3,7 @@ include(FetchContent)
 FetchContent_Declare(
     googlebenchmark
     GIT_REPOSITORY https://github.com/google/benchmark.git
-    GIT_TAG v1.6.1
+    GIT_TAG v1.7.0
 )
 
 FetchContent_GetProperties(googlebenchmark)

examples/test_itp.cc

@@ -5,8 +5,7 @@ Opensmt*
 pre()
 {
     auto config = std::make_unique<SMTConfig>();
-    const char* msg;
-    config->setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+    config->setOption(SMTConfig::o_produce_inter, SMTOption(true));
     Opensmt* osmt = new Opensmt(opensmt_logic::qf_lra, "test solver", std::move(config));
     return osmt;
 }
@@ -50,8 +49,7 @@ int main()
     {
         printf("unsat\n");
         // Set labeling function
-        const char* msg;
-        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0), msg);
+        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0));
 
         auto itp_context = mainSolver.getInterpolationContext();
         // Create the partitioning mask

examples/test_lra_itp.cc

@@ -5,8 +5,7 @@ Opensmt*
 pre()
 {
     auto config = std::make_unique<SMTConfig>();
-    const char* msg;
-    config->setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+    config->setOption(SMTConfig::o_produce_inter, SMTOption(true));
     Opensmt* osmt = new Opensmt(opensmt_logic::qf_lra, "test solver", std::move(config));
     return osmt;
 }
@@ -57,8 +56,7 @@ int main()
     {
         printf("unsat\n");
         // Set labeling function
-        const char* msg;
-        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0), msg);
+        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0));
         // Create the proof graph
         auto itp_context = mainSolver.getInterpolationContext();
 

examples/test_lra_value.cc

@@ -5,8 +5,7 @@ Opensmt*
 pre()
 {
     auto config = std::unique_ptr<SMTConfig>(new SMTConfig());
-    const char* msg;
-    config->setOption(SMTConfig::o_produce_inter, SMTOption(true), msg);
+    config->setOption(SMTConfig::o_produce_inter, SMTOption(true));
     Opensmt* osmt = new Opensmt(opensmt_logic::qf_lra, "test solver", std::move(config));
     return osmt;
 }
@@ -90,8 +89,7 @@ int main()
     {
         printf("unsat\n");
         // Set labeling function
-        const char* msg;
-        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0), msg);
+        c.setOption(SMTConfig::o_itp_bool_alg, SMTOption(0));
 
         auto itp_context = mainSolver.getInterpolationContext();
         // Create the partitioning mask

regression/QF_BV/bar.smt2.expected.out

@@ -1 +1 @@
-At line 4: syntax error, unexpected TK_SYM, expecting TK_NUM or ')'
+At line 4: syntax error, unexpected TK_SYM, expecting TK_INT or ')'

regression/QF_LRA/clocksynchro_3clocks.worst_case_skew.induct_delta_1.smt2

@@ -1,4 +1,4 @@
-(set-option :ghost-vars 1)
+(set-option :ghost-vars true)
 (set-logic QF_LRA)
 (declare-fun v17 () Real)
 (declare-fun v23 () Real)

regression/QF_UF/distinct_model_1.smt2

@@ -0,0 +1,10 @@
+(set-logic QF_UF)
+(declare-sort U 0)
+(declare-fun c1 () U)
+(declare-fun c2 () U)
+(declare-fun c3 () U)
+(assert (not (= c1 c2)))
+(assert (not (= c1 c3)))
+(assert (not (= c2 c3)))
+(check-sat)
+(get-value ((distinct c1 c2 c3)))

regression/QF_UF/distinct_model_1.smt2.expected.out

@@ -0,0 +1,2 @@
+sat
+(((distinct c1 c2 c3) true))

regression/QF_UF/distinct_model_2.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(declare-sort U 0)
+(declare-fun c1 () U)
+(declare-fun c2 () U)
+(declare-fun c3 () U)
+(assert (distinct c1 c2 c3))
+(assert (= c2 c3))
+(check-sat)

regression/QF_UF/distinct_model_2.smt2.expected.out

@@ -0,0 +1 @@
+unsat

regression/QF_UFLRA/regression_12.smt2

@@ -0,0 +1,6 @@
+(set-logic QF_UFLRA)
+(set-info :status sat)
+(declare-fun f (Real) Real)
+(declare-fun x () Real)
+(assert (and (>= (f 1.0) 0) (< (- x) 0) (= (f x) (- 1))))
+(check-sat)

regression/QF_UFLRA/regression_12.smt2.expected.out

@@ -0,0 +1 @@
+sat

regression/generic/let-overload.smt2

@@ -0,0 +1,4 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(assert (let ((l false) (l true)) l))
+(check-sat)

regression/generic/let-overload.smt2.expected.out

@@ -0,0 +1 @@
+sat

regression/generic/let-overload2.smt2

@@ -0,0 +1,4 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(assert (let ((l true) (l false)) l))
+(check-sat)

regression/generic/let-overload2.smt2.expected.out

@@ -0,0 +1 @@
+unsat

regression/generic/pre-logic.smt2.expected.out

@@ -6,30 +6,30 @@ success
 success
 success
 success
-success
+(error "Overflow in #xdeafbeef")
+
 success
 success
 true
 quux
 Longer story
 3
 /dev/null
-(error "No value for attr :foo-option")
-
+()
 0
-3.14159
-3736059631
+3.141593
+(error "No value for option :hex")
+
 85
-( foo string 10 4075 1.23 2 ( ( ) bar ( :keyword ) ) )
-(error "No value for attr :non-existing-option")
+(foo string #b1010 #xfeb 1.23 2 (() bar (:keyword)))
+(error "No value for option :non-existing-option")
 
 success
 success
 success
 success
 success
-(error "no value for info :foo")
-
+:foo ()
 :error-behavior commit-adultery
 :name OpenSMT
 :authors Muumi-peikko

regression_itp/LIA/lia_itp_split.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

regression_itp/LIA/lia_itp_test.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

regression_itp/LIA/lia_itp_test2.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

regression_itp/LIA/lia_itp_test3.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

regression_itp/bug_mask_ite.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 
 (declare-fun x () Real)

regression_itp/bug_mask_ite_nested.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun |state::state.pc| () Real)
 (declare-fun |state::state.old| () Real)

regression_itp/dec-far1.smt2

@@ -1,7 +1,7 @@
 (set-option :produce-interpolants true)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
-(set-option :interpolation-lra-algorithm 4) ; decomposed Farkas
+(set-option :interpolation-lra-algorithm 11) ; decomposed Farkas
 (declare-fun x1 () Real)
 (declare-fun x2 () Real)
 (declare-fun x3 () Real)

regression_itp/dec-far2.smt2

@@ -1,7 +1,7 @@
 (set-option :produce-interpolants true)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
-(set-option :interpolation-lra-algorithm 4) ; decomposed Farkas
+(set-option :interpolation-lra-algorithm 11) ; decomposed Farkas
 (declare-fun x1 () Real)
 (declare-fun x2 () Real)
 (declare-fun x3 () Real)

regression_itp/distinct_unsat.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (set-info :status unsat)
 (declare-fun a () Real)

regression_itp/incremental/inc_itp_theory_prop.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun x () Real)
 (push 1)

regression_itp/incremental/incremental_itp.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun b () Bool)
 (assert (!

regression_itp/incremental/incremental_itp2.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun a () Real)
 (assert (!

regression_itp/incremental/incremental_itp3.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

regression_itp/incremental/incremental_itp4.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_UF)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

regression_itp/incremental/incremental_itp5.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_UF)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

regression_itp/incremental/issue152_itp.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LRA)
 (declare-fun r11 () Real)
 (check-sat)

regression_itp/incremental/lia_splits.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

regression_itp/incremental/lia_splits2.smt2

@@ -1,4 +1,4 @@
-(set-option :produce-interpolants 1)
+(set-option :produce-interpolants true)
 (set-logic QF_LIA)
 (declare-fun x () Int)
 (declare-fun y () Int)

regression_itp/itp_bug.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun |state_type::state.delta| () Real)
 (declare-fun |state_type::state.v!0| () Real)

regression_itp/itp_bug_small.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun x () Bool)
 

regression_itp/part_bug.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_LRA)
 (declare-fun |hifrog::fun_start!0#3| () Bool)
 (declare-fun |hifrog::fun_end!0#3| () Bool)

regression_itp/preint-options.smt2

@@ -1,4 +1,4 @@
 (set-logic QF_LRA)
 (set-option :produce-interpolants true)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (check-sat)

regression_itp/proof_duplicate_literals.smt2

@@ -1,8 +1,8 @@
-(set-option :produce-interpolants 1)
-(set-option :proof-reduce 1)
-;(set-option :proof-check 1)
+(set-option :produce-interpolants true)
+(set-option :proof-reduce true)
+;(set-option :proof-check true)
 ;(set-option :verbosity 2)
-(set-option :certify-interpolants 1)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-fun a () Bool)
 (declare-fun b () Bool)

regression_itp/trivial-proof-A.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-fun x () Bool)
 (assert (! false :named A))

regression_itp/trivial-proof-B.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-fun x () Bool)
 (assert (! x :named A))

regression_itp/uf-itp-edge-split.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort U 0)
 (declare-fun p () Bool)

regression_itp/uf_bug.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort U 0)
 (declare-fun e () U)

regression_itp/uf_duplicates.smt2

@@ -1,5 +1,5 @@
-(set-option :produce-interpolants 1)
-(set-option :certify-interpolants 1)
+(set-option :produce-interpolants true)
+(set-option :certify-interpolants true)
 (set-logic QF_UF)
 (declare-sort Real 0)
 (declare-fun .uf-not () Bool)