mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

test

Browse source
This commit is contained in:
Lev Nachmanson 2024-12-20 12:40:59 -10:00 • committed by Lev Nachmanson
parent 7ecac27335
commit bef313f7a0
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/dioph_eq.cpp
View file

@ -11,7 +11,8 @@
#include "math/lp/lp_utils.h"
/*
Following paper: "A Practical Approach to Satisfiability Modulo Linear
Integer Arithmetic" by Alberto Griggio(griggio@fbk.eu) Data structures are:
Integer Arithmetic" by Alberto Griggio(griggio@fbk.eu).
Data structures are:
-- term_o: inherits lar_term and differs from it by having a constant, while
lar_term is just a sum of monomials
-- entry : has a dependency lar_term, keeping the history of the entry