yices requires logic be set explicitly

Fault-lang · Mar 4, 2023 · 36be545 · 36be545
1 parent 4d966f9
commit 36be545
Show file tree

Hide file tree

Showing 21 changed files with 48 additions and 15 deletions.
diff --git a/smt/asserts_test.go b/smt/asserts_test.go
@@ -25,7 +25,8 @@ func TestSimpleAssert(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -74,7 +75,8 @@ func TestCompoundAssertAnd(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -133,7 +135,8 @@ func TestCompoundAssertOr(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -182,7 +185,8 @@ func TestMultiAssert(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -247,7 +251,8 @@ func TestAssertInfix(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -301,7 +306,8 @@ func TestMultiVar(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_fuzz_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
@@ -357,7 +363,8 @@ func TestSimpleAssume(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -406,7 +413,8 @@ func TestSpecificStateAssume(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)

diff --git a/smt/generator.go b/smt/generator.go
@@ -1497,6 +1497,7 @@ func (g *Generator) tempRule(inst value.Value, r rules.Rule) {
 func (g *Generator) SMT() string {
 	var out bytes.Buffer
 
+	out.WriteString("(set-logic QF_NRA)")
 	out.WriteString(strings.Join(g.inits, "\n"))
 	out.WriteString(strings.Join(g.constants, "\n"))
 	out.WriteString(strings.Join(g.rules, "\n"))

diff --git a/smt/generator_test.go b/smt/generator_test.go
@@ -39,7 +39,8 @@ func TestEventually(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -88,7 +89,8 @@ func TestEventuallyAlways(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -144,7 +146,8 @@ func TestEventuallyAlways2(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -200,7 +203,8 @@ func TestTemporal(t *testing.T) {
 		t.bar;
 	};
 	`
-	expecting := `(declare-fun test1_t_foo_value_0 () Real)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_t_foo_value_0 () Real)
 	(declare-fun test1_t_foo_value_1 () Real)
 	(declare-fun test1_t_foo_value_2 () Real)
 	(declare-fun test1_t_foo_value_3 () Real)
@@ -253,7 +257,7 @@ func TestTemporal2(t *testing.T) {
 			t.bar;
 		};
 	`
-	expecting := `
+	expecting := `(set-logic QF_NRA)
 	(declare-fun test1_a_0 () Real)
 (declare-fun test1_b_0 () Real)
 (declare-fun test1_t_u_x_0 () Real)
@@ -311,7 +315,8 @@ func TestTemporalSys(t *testing.T) {
 			a: zoo,
 		};
 		`
-	expecting := `(declare-fun test1_b_bar_2 () Bool)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_b_bar_2 () Bool)
 	(declare-fun test1_a_foo_2 () Bool)
 	(declare-fun test1_a_foo_4 () Bool)
 	(declare-fun test1_a_zoo_3 () Bool)
@@ -390,7 +395,8 @@ func TestTemporalSys2(t *testing.T) {
 
 		for 2 run{};
 		`
-	expecting := `(declare-fun test1_b_bar_2 () Bool)
+	expecting := `(set-logic QF_NRA)
+	(declare-fun test1_b_bar_2 () Bool)
 	(declare-fun test1_a_foo_2 () Bool)
 	(declare-fun test1_a_zoo_3 () Bool)
 	(declare-fun test1_a_foo_4 () Bool)

diff --git a/smt/testdata/bathtub.smt2 b/smt/testdata/bathtub.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun bathtub_drawn_water_level_0 () Real)
 (declare-fun bathtub_pipe_water_level_0 () Real)
 (declare-fun bathtub_drawn_water_level_1 () Real)

diff --git a/smt/testdata/bathtub2.smt2 b/smt/testdata/bathtub2.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun bathtub_drawn_water_level_0 () Real)
 (declare-fun bathtub_drawn_water_level_1 () Real)
 (declare-fun bathtub_drawn_water_level_2 () Real)

diff --git a/smt/testdata/booleans.smt2 b/smt/testdata/booleans.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun booleans_l_vault_value_0 () Bool)
 (declare-fun booleans_l_vault_value_3 () Bool)
 (declare-fun booleans_l_vault_value_1 () Bool)

diff --git a/smt/testdata/conditionals/condwelse.smt2 b/smt/testdata/conditionals/condwelse.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun condwe_t_base_value_2 () Real)
 (declare-fun condwe_t_base_value_4 () Real)
 (declare-fun condwe_t_base_cond_0 () Real)

diff --git a/smt/testdata/conditionals/multicond.smt2 b/smt/testdata/conditionals/multicond.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun multicond_t_base_cond_0 () Real)
 (declare-fun multicond_t_base_value_0 () Real)
 (declare-fun multicond_t_base_value_2 () Real)

diff --git a/smt/testdata/conditionals/multicond2.smt2 b/smt/testdata/conditionals/multicond2.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun multicond_t_base_value_2 () Real)
 (declare-fun multicond_t_base_cond_0 () Real)
 (declare-fun multicond_t_base_value_0 () Real)

diff --git a/smt/testdata/conditionals/multicond3.smt2 b/smt/testdata/conditionals/multicond3.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun multicond_t_base_value_2 () Real)
 (declare-fun multicond_t_base_value_3 () Real)
 (declare-fun multicond_t_base_cond_2 () Real)

diff --git a/smt/testdata/conditionals/multicond4.smt2 b/smt/testdata/conditionals/multicond4.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun multicond_t_base_value_2 () Real)
 (declare-fun multicond_t_base_value_3 () Real)
 (declare-fun multicond_t_base_cond_2 () Real)

diff --git a/smt/testdata/conditionals/multicond5.smt2 b/smt/testdata/conditionals/multicond5.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun multicond_t_base_value_3 () Real)
 (declare-fun multicond_t_base_value_4 () Real)
 (declare-fun multicond_t_base_value_5 () Real)

diff --git a/smt/testdata/multifile1.smt2 b/smt/testdata/multifile1.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun multifile1_servers_pool_vm1_cpu_0 () Real)
 (declare-fun multifile1_servers_pool_vm1_memory_0 () Real)
 (declare-fun multifile1_servers_pool_vm2_cpu_0 () Real)

diff --git a/smt/testdata/simple.smt2 b/smt/testdata/simple.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun simple_l_active_0 () Bool)
 (declare-fun simple_l_vault_value_0 () Real)
 (declare-fun simple_l_vault_value_2 () Real)

diff --git a/smt/testdata/statecharts/advanceand.smt2 b/smt/testdata/statecharts/advanceand.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun adand_a_option1_1 () Bool)
 (declare-fun adand_a_choice_2 () Bool)
 (declare-fun adand_a_option2_1 () Bool)

diff --git a/smt/testdata/statecharts/advanceor.smt2 b/smt/testdata/statecharts/advanceor.smt2
@@ -1,4 +1,5 @@
 
+(set-logic QF_NRA)
 (declare-fun ador_a_option1_1 () Bool)
 (declare-fun ador_a_choice_2 () Bool)
 (declare-fun ador_a_option2_1 () Bool)

diff --git a/smt/testdata/statecharts/mixedcalls.smt2 b/smt/testdata/statecharts/mixedcalls.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun mixed_a_option2_1 () Bool)
 (declare-fun mixed_a_choice_2 () Bool)
 (declare-fun mixed_a_option3_1 () Bool)

diff --git a/smt/testdata/statecharts/multioradvance.smt2 b/smt/testdata/statecharts/multioradvance.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun ador_a_option1_1 () Bool)
 (declare-fun ador_a_choice_2 () Bool)
 (declare-fun ador_a_option2_1 () Bool)

diff --git a/smt/testdata/statecharts/statechart.smt2 b/smt/testdata/statecharts/statechart.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun statechart_fl_vault_value_2 () Real)
 (declare-fun statechart_fl_vault_value_3 () Real)
 (declare-fun statechart_drain_open_2 () Bool)

diff --git a/smt/testdata/statecharts/triggerfunc.smt2 b/smt/testdata/statecharts/triggerfunc.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun trigger_fl_vault_value_2 () Real)
 (declare-fun trigger_fl_vault_value_3 () Real)
 (declare-fun trigger_fl_vault_value_5 () Real)

diff --git a/smt/testdata/unknowns.smt2 b/smt/testdata/unknowns.smt2
@@ -1,3 +1,4 @@
+(set-logic QF_NRA)
 (declare-fun unknowns_loop_data_a_0 () Real)
 (declare-fun unknowns_loop_data_b_0 () Real)
 (declare-fun unknowns_loop_data_c_0 () Real)