Stack Overflow
Stack Overflow

Questions tagged [mathsat]

MathSAT 5, an efficient Satisfiability modulo theories (SMT) solver.

MathSAT 5, an efficient Satisfiability modulo theories (SMT) solver. MathSAT 5 is the successor of MathSAT 4, supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).

MathSAT 5 is a joint project of Fondazione Bruno Kessler and DISI-University of Trento.

8 questions
3
votes
2 answers

Executing get-model or unsat-core depending on solver's decision

I wonder, if there is a possibility in a SMT-LIB 2.0 script to access the last satisfiability decision of a solver (sat, unsat, ...). For example, the following code: (set-option :produce-unsat-cores true) (set-option :produce-models…
Mr 525
  • 75
  • 8
1
vote
1 answer

What conversion operators are available in Z3 and CVC4 for Bit-Vectors?

I am writing a BV encoding of a problem which requires converting some Int to BitVec and viceversa. In mathsat/optimathsat one can use: ((_ to_bv BITS) ) ; Int => BitVec (sbv_to_int ) ; Signed BitVec => Int (ubv_to_int…
Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
1
vote
2 answers

How to use Z3 and CVC4 with SMT -LIB to prove theorems for the dihedral group D3

In a previous post one theorem for the dihedral group D3 using Z3 SMT-LIB was proved. In this post we try to prove such theorem using both Z3 and CVC4 using the following SMT-LIB code: (set-logic AUFNIRA) (set-option :produce-models…
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
1
vote
1 answer

How to determine the number of solutions of a given instance using Mathsat

Mathsat supports the command check-allsat and Z3 does not support it. Please consider the following example: (declare-fun m () Bool) (declare-fun p () Bool) (declare-fun b () Bool) (declare-fun c () Bool) (declare-fun r () Bool) (declare-fun al ()…
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
1
vote
1 answer

How to execute the following SMT-LIB code using Alt-Ergo

The following SMT-LIB code runs without problems in Z3, MathSat and CVC4 but it is not running in Alt-Ergo, please let me know what happens, many thanks: (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true) (declare-fun…
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
0
votes
0 answers

arm-linux-gnueabi-g++: .so file not recognized

I would like to compile MathSat on an EV3 Mindstorm with ev3dev as OS. For this, I am using the installer given by PySMT (PySMT is successfully installed): pysmt-install --msat Additionally, I installed some necessary packages: sudo apt-get install…
Steve2Fish
  • 187
  • 4
  • 15
0
votes
1 answer

Kaggle Dataset - Letter and numbers meaning

I have come across some data on Kaggle. https://www.itl.nist.gov/div898/strd/nls/data/LINKS/DATA/MGH09.dat I am trying to insert this to excel by copy and pasting it. What do the letters and numbers mean? How would this data look once it was…
Luke
  • 29
  • 8
0
votes
1 answer

Can z3 read the outputfile of MathSAT as its inputfile?

I need to conduct some experiments using z3 and mathsat. I have already finished the experiments with mathsat. It takes a lot of time to write the input file for mathsat and I don't want to write the input files for z3 again. Mathsat supports…
Dingbao Xie
  • 716
  • 9
  • 21